loc:Id, k:Knd, L:IdLnk List. @loc: k sends only on links in L  Realizer 

latex

Definitions	x:A. B(x), t  T, Realizer, @loc: k sends only on links in L, Prop, x. t(x), x(s)
Lemmas	Id wf, fpf wf, decl-state wf, Knd wf, IdLnk wf, decl-type wf, unit wf